-
Notifications
You must be signed in to change notification settings - Fork 106
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
verification for IOAPIC PR seL4/seL4#896 #753
Conversation
0d9a0a2
to
ad180ed
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good to me (assuming that the Word_Lib
failure is trivial)!
Did the new invariant in valid_arch_state'
really not need any proof updates to show that it's maintained? I'm actually pretty impressed if so, even with it only depending on such specific parts of the state, I would have thought that some of the higher level functions would need at least some manual steps to show it.
It should be, I moved the lemma manually without checking dependencies, and that's what I get for my laziness :-)
I was also pretty impressed. AFAICS it works, because I managed to export the state dependency via abbreviation and therefore the lifting rule for |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Cool, another long-standing seL4 PR closed.
5175d01
to
4cae0a9
Compare
The Word_Lib failure has drawn in a whole slate of word lemma movement from CRefine, so it's probably worth looking at this again before I merge. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm confused by the remaining failures but assuming that it's mostly unrelated then it still looks good to me.
They were because the seL4 PR was not rebased yet and didn't have some of the hyp related changes that happened in the meantime. I've pushed a rebased version of the PR and restarted the tests. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Approved v2, very nice, and I appreciate the emptying of Move_C.
Super minor nitpick:
x64 ainvs+refine: ioapic_nirqs proof updates
but
x64 crefine: ioapic_nirqs updates
Separate IOAPICs can have different max numbers of IRQs. This PR adds the logic of seL4/seL4#896 for that to the specs. Signed-off-by: Gerwin Klein <[email protected]>
Slighly weaken arch_irq_control_inv_valid -- the condition `pin < ioapicIRQLines` was unused and would now require a new state invariant on x64_ioapic_nirqs to prove. Signed-off-by: Gerwin Klein <[email protected]>
Place constraints on the new IOPAPIC state components x64KSNumIOAPICs and x64KSIOAPICnIRQs to support CRefine arithmetic. Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
Signed-off-by: Gerwin Klein <[email protected]>
seL4/seL4#896 changes IOAPIC-related decoding slightly and requires a few new small invariants on the Haskell level.
Test with: seL4/seL4#896